
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Backend.Model.ErgoBackendRuntime</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Backend.Model.ErgoBackendRuntime" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Backend.Model.ErgoBackendRuntime</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Closure.html">Qcert.Utils.Closure</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.CommonSystem.html">Qcert.Common.CommonSystem</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Compiler.Model.CompilerRuntime.html">Qcert.Compiler.Model.CompilerRuntime</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJavaScript.html">Qcert.Translation.NNRCtoJavaScript</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.cNNRC.Lang.cNNRC.html">Qcert.cNNRC.Lang.cNNRC</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.DateTimeModelPart.html">ErgoSpec.Backend.Model.DateTimeModelPart</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html">ErgoSpec.Backend.Model.ErgoEnhancedModel</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ForeignErgo.html">ErgoSpec.Backend.ForeignErgo</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendModel.html">ErgoSpec.Backend.Model.ErgoBackendModel</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="id"><a name="ErgoBackendRuntime">ErgoBackendRuntime</a></span> &lt;: <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendModel.html#ErgoBackendModel">ErgoBackendModel</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ErgoBackendRuntime.ergo_foreign_data">ergo_foreign_data</a></span> := <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#enhanced_foreign_data">enhanced_foreign_data</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ErgoBackendRuntime.ergo_data_to_json_string">ergo_data_to_json_string</a></span> := <span class="id"><a href="https://querycert.github.io/html/Qcert.Translation.NNRCtoJavaScript.html#dataToJS">NNRCtoJavaScript.dataToJS</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ErgoBackendRuntime.ergo_foreign_type">ergo_foreign_type</a></span> := <span class="id"><a href="ErgoSpec.Backend.Model.ErgoEnhancedModel.html#enhanced_foreign_type">enhanced_foreign_type</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Backend.Model.ErgoBackendRuntime.html#ErgoBackendRuntime">ErgoBackendRuntime</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
